Lean 4でHello World - pogi-log

Lean 4でHello World

elanを入れる

インストールはelanのページを見る

https://leanprover.github.io/lean4/doc/setup.html

lean 4エラーメモ

下のサンプルを参考にした方が良い。

$ git clone https://github.com/leanprover/lean4-samples

lean4-samples/README.md at main · leanprover/lean4-samples · GitHub

lean4-samples/HelloWorld/lakefile.lean at main · leanprover/lean4-samples · GitHub

うまくいかなかったとき

code:memo

PS C:\Users\alles\workspace\ghworkspace\language\lean\my-lean-proj> lake build

error: dependency mathlib of myleanproj not in manifest, use lake update to update

PS C:\Users\alles\workspace\ghworkspace\language\lean\my-lean-proj> lake update

cloning https://github.com/leanprover-community/mathlib4 to lake-packages\mathlib

cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets

cloning https://github.com/gebner/quote4 to .\lake-packages\Qq

cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop

cloning https://github.com/leanprover/std4 to .\lake-packages\std

うまくいったとき

code:memo

lake build

0/2 Building Main

stdout:

Hello, world!

"4.0.0-nightly-2023-06-08"

1/2 Compiling Main

2/2 Linking test.exe

============================

lakeリポジトリのページに沿ってやったら普通にできた。

leanprover/lake: Lean 4 build system and package manager with configuration files written in Lean. **(Merged into Lean 4.)**

メモ

Extended Setup Notes - Lean Manual